(*
 * Copyright 2014, NICTA
 *
 * This software may be distributed and modified according to the terms of
 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
 * See "LICENSE_BSD2.txt" for details.
 *
 * @TAG(NICTA_BSD)
 *)

(* Tracing debug. *)
val should_debug = Unsynchronized.ref false
fun debug_trace s =
  if (!should_debug) then
    tracing s
  else
    ()

fun funkysplit [_,b,c] = [b,c]
        | funkysplit [_,c] = [c]
        | funkysplit l = l

fun real_base_name name = name |> Long_Name.explode |> funkysplit |> Long_Name.implode (*Handles locales properly-ish*)

fun handle_int exn func = if Exn.is_interrupt exn then reraise exn else func

val wp_sect = "wp";
val ignore_sect = "ignore";
val simp_sect = "simp";
val lift_sect = "lift";
val ignore_del_sect = "ignore_del";
val unfold_sect = "unfold";

fun read_const ctxt = Proof_Context.read_const {proper = true, strict = false} ctxt;

signature CrunchInstance =
sig
    type extra;
    val name : string;
    val has_preconds : bool;
    val mk_term : term -> term -> extra -> term;
    val get_precond : term -> term;
    val put_precond : term -> term -> term;
    val pre_thms : thm list;
    val wpc_tactic : Proof.context -> tactic;
    val parse_extra : Proof.context -> string -> term * extra;
    val magic : term;
end

signature CRUNCH =
sig
    type extra;
    (* Crunch configuration: theory, naming scheme, lifting rules, wp rules *)
    type crunch_cfg = {ctxt: local_theory, prp_name: string, nmspce: string option, lifts: thm list,
        wps: (string * thm) list, igs: string list, simps: thm list, ig_dels: string list, unfolds: (string * thm) list};

    (* Crunch takes a configuration, a precondition, any extra information needed, a debug stack,
    a constant name, and a list of previously proven theorems, and returns a theorem for
    this constant and a list of new theorems (which may be empty if the result
    had already been proven). *)
    val crunch :
       crunch_cfg -> term -> extra -> string list -> string
         -> (string * thm) list ->  (thm option * (string * thm) list);

    val crunch_x : Token.src list -> string -> string -> (string * xstring) list
         -> string list -> local_theory -> local_theory;

    val crunch_ignore_add_del : string list -> string list -> theory -> theory
end

functor Crunch (Instance : CrunchInstance) =
struct

type extra = Instance.extra;

type crunch_cfg = {ctxt: local_theory, prp_name: string, nmspce: string option, lifts: thm list,
    wps: (string * thm) list, igs: string list, simps: thm list, ig_dels: string list, unfolds: (string * thm) list};

structure CrunchIgnore = Generic_Data
(struct
    type T = string list
    val empty = []
    val extend = I
    val merge = Library.merge (op =);
end);

fun crunch_ignore_add thms thy =
  Context.theory_map (CrunchIgnore.map (curry (Library.merge (op =)) thms)) thy

fun crunch_ignore_del thms thy =
  Context.theory_map (CrunchIgnore.map (Library.subtract (op =) thms)) thy

fun crunch_ignore_add_del adds dels thy =
  thy |> crunch_ignore_add adds |> crunch_ignore_del dels

val def_sfx = "_def"; 
val induct_sfx = ".induct";
val simps_sfx = ".simps";
val param_name = "param_a";
val dummy_monad_name = "__dummy__";

fun def_of n = n ^ def_sfx;
fun induct_of n = n ^ induct_sfx;
fun simps_of n = n ^ simps_sfx;

fun num_args t = length (binder_types t) - 1;

fun real_const_from_name const nmspce ctxt =
    let
      val qual::locale::nm::nil = Long_Name.explode const;
      val SOME some_nmspce = nmspce;
      val nm = Long_Name.implode (some_nmspce :: nm :: nil);
      val _ = read_const ctxt nm;
     in
       nm
     end
     handle exn => handle_int exn const;


fun get_monad ctxt f xs = if is_Const f then
    (* we need the type of the underlying constant to avoid polymorphic
       constants like If, case_option, K_bind being considered monadic *)
    let val T = dest_Const f |> fst |> read_const ctxt |> type_of;

    fun is_product v (Type ("Product_Type.prod", [Type ("fun", [Type ("Product_Type.prod", [_,v']), Type ("HOL.bool",[])]), Type ("HOL.bool",[])])) = (v = v')
      | is_product v (Type ("Product_Type.prod", [Type ("Set.set", [Type ("Product_Type.prod", [_,v'])]), Type ("HOL.bool",[])])) = (v = v')
      | is_product _ _ = false;

    fun num_args (Type ("fun", [v,p])) n =
          if is_product v p then SOME n else num_args p (n + 1)
      | num_args _ _ = NONE
        
    in case num_args T 0 of NONE => []
      | SOME n => [list_comb (f, Library.take n (xs @ map Bound (1 upto n)))]
    end
  else [];

fun monads_of ctxt t = case strip_comb t of
    (Const f, xs) => get_monad ctxt (Const f) xs @ maps (monads_of ctxt) xs
  | (Abs (_, _, t), []) => monads_of ctxt t
  | (Abs a, xs) => monads_of ctxt (betapplys (Abs a, xs))
  | (_, xs) => maps (monads_of ctxt) xs;


val get_thm = Proof_Context.get_thm

val get_thms = Proof_Context.get_thms

fun maybe_thms thy name = get_thms thy name handle exn => handle_int exn []
fun thy_maybe_thms thy name = Global_Theory.get_thms thy name handle exn => handle_int exn []

fun add_thm thm atts name ctxt =
  Local_Theory.notes [((Binding.name name, atts), [([thm], atts)])] ctxt |> #2

fun get_thm_name_bluh (cfg: crunch_cfg) const_name
  = Long_Name.base_name const_name ^ "_" ^ (#prp_name cfg)

fun get_thm_name (cfg : crunch_cfg) const_name
  = if read_const (#ctxt cfg) (Long_Name.base_name const_name)
         = read_const (#ctxt cfg) const_name
      then Long_Name.base_name const_name ^ "_" ^ (#prp_name cfg)
      else space_implode "_" (space_explode "." const_name @ [#prp_name cfg])

fun get_stored cfg n = get_thm (#ctxt cfg) (get_thm_name cfg n)

fun get_stored_bluh cfg n = 
  let val r = (maybe_thms (#ctxt cfg) (get_thm_name cfg n)) @ (maybe_thms (#ctxt cfg) (get_thm_name_bluh cfg n));
      in (case r of [] => error ("") | _ => (hd r))
  end

fun mapM _ [] y = y
  | mapM f (x::xs) y = mapM f xs (f x y)

fun dest_equals t = t |> Logic.dest_equals
  handle TERM _ => t |> HOLogic.dest_Trueprop |> HOLogic.dest_eq;

fun const_is_lhs const nmspce ctxt def =
    let
      val (lhs, _) = def |> Thm.prop_of |> dest_equals;
      val (nm, _)  = dest_Const const;
      val (nm', _) = dest_Const (head_of lhs);
    in
      (real_const_from_name nm nmspce ctxt) = (real_const_from_name nm' nmspce ctxt)
    end handle TERM _ => false

fun deep_search_thms ctxt defn const nmspce =
    let
      val thy  = Proof_Context.theory_of ctxt
      val thys = thy :: Theory.ancestors_of thy;
      val filt = filter (const_is_lhs const nmspce ctxt);
    
      fun search [] = error("not found: const: " ^ PolyML.makestring const ^ " defn: " ^ PolyML.makestring defn)
        | search (t::ts) = (case (filt (thy_maybe_thms t defn)) of
              [] => search ts
	    | thms => thms);
    in
      case filt (maybe_thms ctxt defn) of
          [] => search thys
        | defs => defs
     end;

val unfold_get_params = @{thms Let_def return_bind returnOk_bindE
    K_bind_def split_def bind_assoc bindE_assoc
    trans[OF liftE_bindE return_bind]};

fun unfold ctxt const triple nmspce =
    let
      val _ = debug_trace "unfold"
      val const_term = read_const ctxt const;
      val const_defn = const |> Long_Name.base_name |> def_of;
      val const_def = deep_search_thms ctxt const_defn const_term nmspce
                        |> hd |> Simpdata.safe_mk_meta_eq;
      val _ = Pretty.writeln (Pretty.block [Pretty.str ("const_def: " ^ PolyML.makestring const_defn), Display.pretty_thm ctxt const_def])
      val trivial_rule = Thm.trivial triple
      val _ = Pretty.writeln (Pretty.block [Pretty.str "trivial_rule: ", Display.pretty_thm ctxt trivial_rule])
      val unfold_rule = trivial_rule
        |> Simplifier.rewrite_goals_rule ctxt [const_def];
      val _ = Pretty.writeln (Pretty.block [Pretty.str "unfold_rule: ", Display.pretty_thm ctxt unfold_rule])
      val ms = unfold_rule
        |> Simplifier.rewrite_goals_rule ctxt unfold_get_params
        |> Thm.prems_of |> maps (monads_of ctxt);
    in if Thm.eq_thm_prop (trivial_rule, unfold_rule)
       then error ("Unfold rule generated for " ^ const ^ " does not apply")
       else (ms, unfold_rule) end

fun mk_apps t n m = 
    if n = 0 
    then t
    else mk_apps t (n-1) (m+1) $ Bound m

fun mk_abs t n =
    if n = 0
    then t
    else Abs ("_", dummyT, mk_abs t (n-1))

fun eq_cname (Const (s, _)) (Const (t, _)) = (s = t)
  | eq_cname _ _ = false

fun resolve_abbreviated ctxt abbrev =
  let
      val (abbrevn,_) = dest_Const abbrev
      val origin = (head_of (snd ((Consts.the_abbreviation o Proof_Context.consts_of) ctxt abbrevn)));
      val (originn,_) = dest_Const origin;
      val (_::_::_::nil) = Long_Name.explode originn;
    in origin end handle exn => handle_int exn abbrev

fun map_consts f = 
      let
         fun map_aux (Const a) = f (Const a)
           | map_aux (t $ u) = map_aux t $ map_aux u
           | map_aux x = x
      in map_aux end;

fun map_unvarifyT t = map_types Logic.unvarifyT_global t

fun induct_inst ctxt const goal nmspce =
    let
      val _ = debug_trace "induct_inst"
      val base_const = Long_Name.base_name const;
      val _ = debug_trace ("base_const: " ^ PolyML.makestring base_const)
      val induct_thm = base_const |> induct_of |> get_thm ctxt;
      val _ = debug_trace ("induct_thm: " ^ PolyML.makestring induct_thm)
      val const_term = read_const ctxt const |> map_unvarifyT;
      val n = const_term |> fastype_of |> num_args;
      val t = mk_abs (Instance.magic $ mk_apps const_term n 0) n
              |> Syntax.check_term ctxt |> Logic.varify_global |> Thm.cterm_of ctxt;
      val P = Thm.concl_of induct_thm |> HOLogic.dest_Trueprop |> head_of |> Thm.cterm_of ctxt;
      val trivial_rule = Thm.trivial goal;
      val induct_inst = Thm.instantiate ([], [(P, t)]) induct_thm
                        RS trivial_rule;
      val _ = debug_trace ("induct_inst" ^ Syntax.string_of_term ctxt (Thm.prop_of induct_inst));
      val simp_thms = deep_search_thms ctxt (base_const |> simps_of) const_term nmspce;
      val induct_inst_simplified = induct_inst
        |> Simplifier.rewrite_goals_rule ctxt (map Simpdata.safe_mk_meta_eq simp_thms);
      val ms = maps (monads_of ctxt) (Thm.prems_of induct_inst_simplified);
      val ms' = filter_out (eq_cname (resolve_abbreviated ctxt const_term) o head_of) ms;
    in if Thm.eq_thm_prop (trivial_rule, induct_inst)
       then error ("Unfold rule generated for " ^ const ^ " does not apply")
       else (ms', induct_inst) end

fun unfold_data ctxt constn goal nmspce nil = (
    induct_inst ctxt constn goal nmspce handle exn => handle_int exn
    unfold ctxt constn goal nmspce handle exn => handle_int exn
    error ("unfold_data: couldn't find defn or induct rule for " ^ constn))
  | unfold_data ctxt constn goal _ [(_, thm)] =
    let
      val trivial_rule = Thm.trivial goal
      val unfold_rule = Simplifier.rewrite_goals_rule ctxt [safe_mk_meta_eq thm] trivial_rule;
      val ms = unfold_rule
        |> Simplifier.rewrite_goals_rule ctxt unfold_get_params
        |> Thm.prems_of |> maps (monads_of ctxt);
    in if Thm.eq_thm_prop (trivial_rule, unfold_rule)
       then error ("Unfold rule given for " ^ constn ^ " does not apply")
       else (ms, unfold_rule) end
  | unfold_data _ constn _ _ _ = error ("Multiple unfolds are given for " ^ constn)



val split_if = @{thm "split_if"}

fun maybe_cheat_tac ctxt thm =
  if (Goal.skip_proofs_enabled ())
  then ALLGOALS (Skip_Proof.cheat_tac ctxt) thm
  else all_tac thm;

fun var_precond v =
  if Instance.has_preconds
  then Instance.put_precond (Var (("Precond", 0), Instance.get_precond v |> fastype_of)) v
  else v;

fun is_proof_of cfg const (name, _) =
  get_thm_name cfg const = name

fun get_inst_precond ctxt pre extra (mapply, goal) = let
    val (c, xs) = strip_comb mapply;
    fun replace_vars (t, n) =
      if exists_subterm (fn t => is_Bound t orelse is_Var t) t
        then Free ("ignore_me" ^ string_of_int n, dummyT)
      else t
    val ys = map replace_vars (xs ~~ (1 upto (length xs)));
    val goal2 = Instance.mk_term pre (list_comb (c, ys)) extra
      |> Syntax.check_term ctxt |> var_precond
      |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt;
    val spec = goal RS Thm.trivial goal2;
    val precond = Thm.concl_of spec |> HOLogic.dest_Trueprop |> Instance.get_precond;
  in SOME precond end
    (* in rare cases the tuple extracted from the naming scheme doesn't
       match what we were trying to prove, thus a THM exception from RS *)
  handle THM _ => NONE;

fun split_precond (Const (@{const_name pred_conj}, _) $ P $ Q)
    = split_precond P @ split_precond Q
  | split_precond (Abs (n, T, @{const "HOL.conj"} $ P $ Q))
    = maps (split_precond o Envir.eta_contract) [Abs (n, T, P), Abs (n, T, Q)]
  | split_precond t = [t];

val precond_implication_term
  = Syntax.parse_term @{context}
    "%P Q. (!! s. (P s ==> Q s))";

fun precond_needed ctxt pre css pre' = let
    val imp = Syntax.check_term ctxt (precond_implication_term $ pre $ pre');
  in Goal.prove ctxt [] [] imp
       (fn _ => clarsimp_tac css 1); false end
     handle exn => handle_int exn true;

fun combine_preconds ctxt pre pres = let
    val pres' = maps (split_precond o Envir.beta_eta_contract) pres
      |> filter_out (exists_subterm (fn t => is_Var t orelse
            (is_Free t andalso
              is_prefix (op =) (String.explode "ignore_me")
                (String.explode (fst (dest_Free t))))))
      |> remove (op aconv) pre |> distinct (op aconv)
      |> filter (precond_needed ctxt pre ctxt);
    val T = fastype_of pre;
    val conj = Const (@{const_name pred_conj}, T --> T --> T)
  in case pres' of
      [] => pre
    | _ => let val precond = foldl1 (fn (a, b) => conj $ a $ b) pres'
        in if precond_needed ctxt precond ctxt pre then conj $ pre $ precond else precond end
  end;

(* the crunch function is designed to be foldable with this custom fold
   to crunch over a list of constants *)
fun funkyfold _ [] _ = ([], [])
  | funkyfold f (x :: xs) thms = let
    val (z, thms') = f x thms
    val (zs, thms'') = funkyfold f xs (thms' @ thms)
  in (z :: zs, thms' @ thms'') end

exception WrongType

fun make_goal const_term const pre extra ctxt =
  let val nns = const_term |> fastype_of |> num_args |> 
                          Name.invent Name.context param_name; 
      val parse = Syntax.parse_term ctxt;
      val check = Syntax.check_term ctxt;
      val body = parse (String.concat (separate " " (const :: nns)));
  in check (Instance.mk_term pre body extra) end;

fun crunch cfg pre extra stack const' thms =
  let 
    val ctxt = #ctxt cfg |> Context_Position.set_visible false;
    val const = real_const_from_name const' (#nmspce cfg) ctxt;
    val empty_ref = Unsynchronized.ref [] : thm list Unsynchronized.ref (* FIXME: avoid refs *)
  in
    let
      val _ = "crunching constant: " ^ const |> writeln;
      val const_term = read_const ctxt const;
      val real_const_term = resolve_abbreviated ctxt const_term;
      val goal = make_goal const_term const pre extra ctxt
                 handle exn => handle_int exn (raise WrongType);
      val goal_prop = HOLogic.mk_Trueprop goal;
    in
      let val v = find_first (is_proof_of cfg const) thms
      in (SOME (snd (the v)), []) end
      handle exn => handle_int exn
        (SOME (get_stored cfg const), [])
      handle exn => handle_int exn
      let val const_long_name = real_const_term |> dest_Const |> fst;
        val cgoal_prop = Thm.cterm_of ctxt goal_prop;
        val v = find_first (fn (s, t) => s = const_long_name andalso
                    (is_some o SINGLE (WeakestPre.apply_rules_tac_n false ctxt [t] empty_ref 1)) (Goal.init cgoal_prop)) (#wps cfg)
      in (SOME (snd (the v)), []) end
      handle exn => handle_int exn
        let
          fun wp rules = WeakestPre.apply_rules_tac_n false ctxt
                                           (map snd (thms @ #wps cfg) @ rules) empty_ref

          val ctxt' = Variable.auto_fixes goal_prop ctxt
          val (thm, thms')
                   = ( Goal.prove ctxt' [] [] goal_prop (fn prems =>
                                  TRY (wp [] 1) THEN TRY (wp (#lifts cfg) 1))
                         |> singleton (Proof_Context.export ctxt' ctxt)
                     , [] )
          handle exn => handle_int exn
            let
              val ctxt' = Variable.auto_fixes goal ctxt;
              val cgoal = goal |> var_precond |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt';
              val unfolds' = filter (fn (a, _) => a = const) (#unfolds cfg)
              val (ms, unfold_rule) = unfold_data ctxt' const cgoal (#nmspce cfg) unfolds'
                |>> map (fn t => (real_const_from_name (fst (dest_Const (head_of t))) (#nmspce cfg) ctxt', t))
                |>> subtract (fn (a, b) => a = (fst b))
                      (subtract (op =) (#ig_dels cfg) (#igs cfg @ CrunchIgnore.get (Context.Proof ctxt')));
              val stack' = const :: stack;
              val _ = if (length stack' > 20) then
                         (writeln "Crunch call stack:";
                          map writeln (const::stack);
                          error("probably infinite loop")) else ();
              val (goals, thms') = funkyfold (crunch cfg pre extra stack') (map fst ms) thms;
              val goals' = map_filter I goals
              val ctxt'' = ctxt' addsimps ((#simps cfg) @ goals')
                  |> Splitter.del_split split_if

              fun collect_preconds pre =
                let val preconds = map_filter (fn (x, SOME y) => SOME (x, y) | (_, NONE) => NONE) (map snd ms ~~ goals) 
                                                    |> map_filter (get_inst_precond ctxt'' pre extra);
                  val precond = combine_preconds ctxt'' (Instance.get_precond goal) preconds;
                in Instance.put_precond precond goal |> HOLogic.mk_Trueprop end;
              val goal_prop2 = if Instance.has_preconds then collect_preconds pre else goal_prop;

              val ctxt''' = ctxt'' |> Variable.auto_fixes goal_prop2
              val _ = writeln ("attempting: " ^ Syntax.string_of_term ctxt''' goal_prop2);
 
            in (Goal.prove ctxt''' [] [] goal_prop2
                  ( (*DupSkip.goal_prove_wrapper *) (fn _ => 
                  rtac unfold_rule 1
                    THEN maybe_cheat_tac ctxt'''
                  THEN ALLGOALS (fn n =>
                    simp_tac ctxt''' n
                    THEN
                    TRY (resolve_tac ctxt''' Instance.pre_thms n)
                    THEN
                    REPEAT_DETERM (
                      wp goals' n
                      ORELSE
                      CHANGED (clarsimp_tac ctxt''' n) 
                      ORELSE
                      assume_tac ctxt''' n
                      ORELSE
                      Instance.wpc_tactic ctxt'''
                      ORELSE
                      safe_tac ctxt'''
                      ORELSE
                      CHANGED (simp_tac ctxt''' n)
                  )))) |> singleton (Proof_Context.export ctxt''' ctxt)
                  handle e => 
                         (writeln "Crunch call stack:";
                          map writeln (const::stack);
                          raise e)
                , thms') end
        in (SOME thm, (get_thm_name cfg const, thm) :: thms') end
    end
    handle WrongType =>
      let val _ = writeln ("The constant " ^ const ^ " has the wrong type and is being ignored")
      in (NONE, []) end
  end 

(*Todo: Remember mapping from locales to theories*)
fun get_locale_origins full_const_names ctxt =
  let
    fun get_locale_origin abbrev = 
      let
        (*Check if the given const is an abbreviation*)
        val (origin,_) = dest_Const (head_of (snd ((Consts.the_abbreviation o Proof_Context.consts_of) ctxt abbrev)));
        (*Check that the origin can be broken into 3 parts (i.e. it is from a locale) *)
        val [_,_,_] = Long_Name.explode origin;
        (*Remember the theory for the abbreviation*)

        val [qual,nm] = Long_Name.explode abbrev                
      in SOME qual end handle exn => handle_int exn NONE
  in fold (curry (fn (abbrev,qual) => case (get_locale_origin abbrev) of
                                        SOME q => SOME q
                                      | NONE => NONE)) full_const_names NONE
  end
 
fun parse_unfold_pair unfold =
  let
    val parse_string = Scan.repeat (Scan.unless ($$ "," || $$ ")") (Scan.one Symbol.not_eof))
    val ((first, second), rem) = ($$ "(" |-- parse_string --| Scan.this_string ", " -- parse_string --| $$ ")") (Symbol.explode unfold)
      handle exn => handle_int exn error "Could not parse unfold data, expected: (const, thm)"
  in if rem = [] then (implode first, implode second)
    else error "Could not parse unfold data, expected: (const, thm)" end

fun crunch_x atts extra prp_name wpigs consts ctxt =
    let
        fun const_name const = dest_Const (read_const ctxt const) |> #1

        val wps' = wpigs |> filter (fn (s,_) => s = wp_sect) |> map #2

        val simps = wpigs |> filter (fn (s,_) => s = simp_sect) |> map #2 
                    |> maps (get_thms ctxt)

        val igs = wpigs |> filter (fn (s,_) => s = ignore_sect) 
                        |> map (const_name o #2)

        val lifts = wpigs |> filter (fn (s,_) => s = lift_sect) |> map #2
                          |> maps (get_thms ctxt)

        val ig_dels = wpigs |> filter (fn (s,_) => s = ignore_del_sect)
                            |> map (const_name o #2)

        fun read_unfold (first, second) = (const_name first, get_thm ctxt second)

        val unfolds = wpigs |> filter (fn (s,_) => s = unfold_sect) |> map #2
                    |> map (read_unfold o parse_unfold_pair)

        fun mk_wp thm = 
           let val ms = Thm.prop_of thm |> monads_of ctxt;
                val m = if length ms = 1 
                        then 
                            hd ms |> head_of |> dest_Const |> fst
                        else 
                            dummy_monad_name;
            in (m, thm) end;

        val wps = maps (get_thms ctxt) wps' |> map mk_wp;
        val full_const_names = map const_name consts;
       
        val nmspce = get_locale_origins full_const_names ctxt;
        val (pre', extra') = Instance.parse_extra ctxt extra

        (* check that the given constants match the type of the given property*)
        val const_terms = map (read_const ctxt) full_const_names;
        val _ = map (fn (const_term, const) => make_goal const_term const pre' extra' ctxt)
                    (const_terms ~~ full_const_names)

        val (_, thms) = funkyfold (crunch {ctxt = ctxt, prp_name = prp_name, nmspce = nmspce, lifts = lifts,
              wps = wps, igs = igs, simps = simps, ig_dels = ig_dels, unfolds = unfolds} pre' extra' [])
            full_const_names [];

        val atts' = map (Attrib.check_src ctxt) atts;

        val ctxt' = fold (fn (name, thm) => add_thm thm atts' name) thms ctxt;
    in
        Pretty.writeln
          (Pretty.big_list "proved:"
                           (map (fn (n,t) =>
                                    Pretty.block
                                      [Pretty.str (n ^ ": "),
                                       Syntax.pretty_term ctxt (Thm.prop_of t)])
                                thms));
        ctxt'
    end

end
(*
structure Crunch_Crunches : CRUNCH = Crunch;
*)
